R-discrete(R)
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.rec1  rec2
== Rinit(loc,T,x,v)=> <loc, x> : case v of inl(a) => tt | inr(a) => ff
== Rframe(loc,T,x,L)=> 
== Rsframe(lnk,tag,L)=> 
== Reffect(loc,ds,knd,T,x,f)=> <loc, x> : case f of inl(a) => tt | inr(a) => ff
== Rsends(ds,knd,T,l,dt,g)=> 
== Rpre(loc,ds,a,T,P)=> 
== Rkframe(loc,k,L)=> 
== Rksframe(loc,k,L)=> 
== Rrframe(loc,x,L)=>  

latex

---

clarification:

R-discrete(R)
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.fpf-join(product-deq(Id;Id;IdDeq;IdDeq);rec1;rec2)
== Rinit(loc,T,x,v)=> <loc, x> : case v of inl(a) => tt | inr(a) => ff
== Rframe(loc,T,x,L)=> 
== Rsframe(lnk,tag,L)=> 
== Reffect(loc,ds,knd,T,x,f)=> <loc, x> : case f of inl(a) => tt | inr(a) => ff
== Rsends(ds,knd,T,l,dt,g)=> 
== Rpre(loc,ds,a,T,P)=> 
== Rkframe(loc,k,L)=> 
== Rksframe(loc,k,L)=> 
== Rrframe(loc,x,L)=>  

latex

Definitions	, ff, tt, case b of inl(x) => s(x) | inr(y) => t(y), <a, b>, x : v, IdDeq, Id, product-deq(A;B;a;b), f  g, es realizer ind
FDL editor aliases	R-discrete